COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00007 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "→"
CS206∂(27)FINAL EXAMINATION→FALL 1977

	This examination is open book and notes.
Write LISP functions as follows except where something else is
requested.  Either notation may be used.
When a requested proof requires induction, be sure and write down
the induction principle appealed to and the specific predicate to
which the induction is applied.

.item←0
#. %2rev x%1 is the "reverse" of the arbitrary S-expression ⊗x.  Thus
%2rev%1 (A.(B.C)) = ((C.B).A).  Note that ⊗rev applied to a list
does not give the usual reversal of the list.

	a. Write a recursive definition of ⊗rev. 

	b. Prove that ⊗rev is total.

	c. Prove that ⊗rev satisfies %2∀x: rev rev x = x%1.

#. We will say that a list ⊗u is "intermittently contained" in
a list ⊗ v if the elements of ⊗u occur in ⊗v in the same order
as in ⊗u but possibly separated by other elements of ⊗v.  We write
%2u_≤≤_v%1 for this relation.  Thus we have  (A_C_E)_≤≤_(X_A_B_C_A_F_D_E_G).

	a. Write a recursive definition of %2u ≤≤ v%1.

Assume, to make the problem easier, that your %2u ≤≤ v%1 is total, and
prove

	b. %2∀u:u << u%1.

	c. %2∀u v w:(u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w)%1.

#. Let ⊗e be a LISP expression in internal notation.  %2usecadr e%1 is
equivalent to ⊗e except that subexpressions of the form (CAR_(CDR_%2e%1)) are
replaced by (CADR_%2e%1).  Thus

	%2usecadr%1 (CONS (CAR (CDR (FOO X))) Y) = (CONS (CADR (FOO X)) Y).

#. What is %2compexp[%1(CONS (CAR X) Y), 0, ((X.1)(Y.2))] as compiled by
LCOM0 and LCOM4.

#. Write an abstract evaluator for Boolean expressions using the
abstract syntactic functions

	a. %2isand e%1 meaning that ⊗e has principal connective "and".

	b. %2isor e%1 meaning that ⊗e has principal connective "or".

	c. %2isnot e%1 meaning that ⊗e has principal connective "not".

	d. In each of the three above cases, %2operands e%1 gives a list
of the operands of the expression.  If ⊗e satisfies %2isnot%1, there is
exactly one operand, but in the other cases there may be any number.  The
LISP functions and predicates qa, qd, qn are applicable to these lists.

	e. %2isvar e%1 means that ⊗e is a Boolean variable, and in this
case the predicate %2true(e,%Ax%1) is true if ⊗e is true in the
state %Ax%1.

	Write a recursive definition of the predicate %2istrue(e,%Ax%1)
whose value is true or false according to whether the Boolean expression
⊗e is true in the state %Ax%1.  Your program should
not look at more terms of "and"s and "or"s than necessary to
decide the truth value.